*****ASSUME A(RW,w,W2,1);

1 A(RW,w,W2,1)  (1)

*****ASSUME color(W2,w)=B;

2 color(W2,w)=B  (2)

*****ASSUME A(w,w1,W1,0);

3 A(w,w1,W1,0)  (3)

*****∀E w12 RW,w,1;

4 (A(RW,w,W1,1)∨A(RW,w,W2,1))⊃A(RW,w,W12,1)  

*****∀E elweka1 w;

5 A(RW,w,W12,1)≡(A(RW,w,W12,0)∧∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(%
p,RW))))  

*****∀E initial2 w,w1;

6 (A(RW,w,W12,0)∧A(w,w1,W1,0))⊃color(W2,w1)=color(W2,w)  

*****∀E king w1;

7 A(RW,w1,W12,0)⊃(color(W1,w1)=W∨color(W2,w1)=W)  

*****∀E transitive RW,w,w1,W12,0;

8 (A(RW,w,W12,0)∧A(w,w1,W12,0))⊃A(RW,w1,W12,0)  

*****∀E w12 w,w1,0;

9 (A(w,w1,W1,0)∨A(w,w1,W2,0))⊃A(w,w1,W12,0)  

*****∀E king w;

10 A(RW,w,W12,0)⊃(color(W1,w)=W∨color(W2,w)=W)  

*****TAUTEQ color(W1,w1)=color(W1,w) color1,1:10;

11 color(W1,w1)=color(W1,w)  (1 2 3)

*****⊃I 3⊃↑;

12 A(w,w1,W1,0)⊃color(W1,w1)=color(W1,w)  (1 2)

*****∀I ↑ w1;

13 ∀w1.(A(w,w1,W1,0)⊃color(W1,w1)=color(W1,w))  (1 2)

*****TAUT ∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW))) 1,4:5;

14 ∀p.(∀w1.(A(w,w1,p,0)⊃color(p,w1)=color(p,w))≡∀w1.(A(RW,w1,p,0)⊃color(p,w1)=color(p,RW)))  (1)

*****∀E ↑ W1;

15 ∀w1.(A(w,w1,W1,0)⊃color(W1,w1)=color(W1,w))≡∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))  (1)

*****TAUT ∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)) 13,15;

16 ∀w1.(A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW))  (1 2)

*****∀E ↑ w1;

17 A(RW,w1,W1,0)⊃color(W1,w1)=color(W1,RW)  (1 2)

*****∀E initial1 B,RW;

18 A(RW,RW,W12,0)⊃(((B=W∨color(W2,RW)=W)⊃∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B))∧((B=W∨color(W1,RW)=W)⊃∃w1.(A(RW,w1,%
W2,0)∧color(W2,w1)=B)))  

*****∀E reflex RW,W12,0;

19 A(RW,RW,W12,0)  

*****TAUT ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B) rw,18:19;

20 ∃w1.(A(RW,w1,W1,0)∧color(W1,w1)=B)  

*****∃E ↑ w1;

21 A(RW,w1,W1,0)∧color(W1,w1)=B  (21)

*****TAUTEQ FALSE rw,color1,17,21;

22 FALSE  (1 2)

*****¬I ↑,color(W2,w)=B;

23 ¬(color(W2,w)=B)  (1)

*****∀E color2 color(W2,w);

24 color(W2,w)=W∨color(W2,w)=B  

*****TAUTEQ color(W2,w)=color(W2,RW) rw,23:24;

25 color(W2,w)=color(W2,RW)  (1)

*****⊃I 1⊃↑;

26 A(RW,w,W2,1)⊃color(W2,w)=color(W2,RW)  

*****∀I ↑ w;

27 ∀w.(A(RW,w,W2,1)⊃color(W2,w)=color(W2,RW))